﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Formality.FormalSystem;

namespace Formality.TestFramework.FormalSystemTestSuite
{
    using P = Proposition;
    using V = Variable;

    public static class Make
    {
        public static P Imp(P l, P r) { return Operators.IMPLIES.Operator(l, r); }
        public static P Or(P l, P r) { return Operators.OR.Operator(l, r); }
        public static P And(P l, P r) { return Operators.AND.Operator(l, r); }
        public static P Ax(P c) { return Operators.AXIOM.Operator(c); }
        public static P Equiv(P l, P r) { return Operators.EQ.Operator(l, r); }
        public static P Def(P l, P r) { return Operators.DEFINED.Operator(l, r); }
        public static P Rule(P c, params P[] a) { return Operators.RULE.Operator(a.Concat(new[] { c })); }
        public static P Not(P p) { return Operators.NOT.Operator(p); }
        public static P ForAll(V Var, P p) { return Operators.FOR_ALL.Binder(Var, p); }
        public static P Exists(V Var, P p) { return Operators.EXISTS.Binder(Var, p); }
        public static P Func(V Var, params V[] Args) { return new Proposition(Var, Args); }
        public static P PFunc(V Var, params V[] Args) { return new Proposition(Var, Args, true); }
    }
}